This invention relates generally to formal verification of circuit designs, and more particularly to static formal verification of circuit designs having properties defined using local variables.
Circuit designs for digital logic are often coded in a Hardware Description Language (HDL), such as SystemVerilog. This code is then verified, or checked for functional correctness. Assertion-based verification (ABV) is a functional verification technique that uses properties, or statements about the behavior of the design, to verify different aspects of the design. Different functional verification tools either monitor or prove the validity of the property, or assertion.
The SystemVerilog language contains a powerful assertion language, called SystemVerilog Assertions (SVA), which is used to write properties. One of the distinguishing features of SVA is the local variable. A local variable is a construct that is used in a sequence or property to store a data value within the property itself. This allows the data value to be compared at a future cycle of the property.
The following simple example illustrates a local variable used in a property that verifies the expected output for a in-order pipeline design with a fixed delay. The local variable is x. When the signal valid_in is asserted, x is assigned and stores the value of the signal pipe_in. Five cycles later, the property is evaluated true if the value of pipe_out1 is x+1; otherwise it is false.
property e; int x; (valid_in, x = pipe_in) | → ##5 (pipe_out1 == (x + 1));endproperty
This simple example contains a local variable that is accessed in order and with a small fixed delay. In dynamic ABV, a new copy of the local variable x is created and initialized for each cycle of simulation whenever valid_in is true. This phenomenon is known as sequence overlap. The value of the local variable is checked five cycles later against pipe_out1, thus giving a maximum limit to the number of outstanding copies of local variable x.
There are different implementation techniques as a result of varying requirements of different verification technologies. Both simulation and dynamic formal verification tools dynamically allocate memory as needed for local variables during verification runtime. In the example above, simulation and dynamic formal verification tools might dynamically allocate memory for at least five copies of the local variable.
Static formal verification tools, in contrast, cannot rely on dynamically allocating memory for SVA variables during run-time. Instead the whole model (circuit design and formal verification specification) is compiled into a statically allocated structure. This means that existing static formal verification tools must be able to determine, during compile time, the number of copies of the local variable needed during verification. For the example above, static formal verification tools can implement a shift register to store the copies of the local variable using the fixed delay.
But it is not always possible for a static verification tool to determine the number of local variables that will be needed. The following complex example illustrates such a situation. This property contains a variable latency with a local variable that is accessed out of order:
property stack_req; logic [stack_width:1] data; logic [counter_width-1:0] mylevel; @ (posedge clk) (push && (pop || !stack_full), data = data_in, mylevel = 0) ##1 (mylevel > 0, mylevel=mylevel+(!stack_full*push-pop)) [*0:$] ##1 (pop && mylevel==0) | = > (data==data_out);endpropertyThis property may be used, for example, to check the correct behavior of a stack. In the property, there are two local variables, data and mylevel. The variable data is used to record some value that is stored on the stack, while the variable mylevel is used to keep track of the relative position of the stack at which the value in question is stored. When there is a push and the stack is not full or there is a simultaneous pull, the value on signal data_in is stored in the local variable data, and the value 0 is stored in the variable mydata. Then, successive pushes and pulls will increment or decrement the variable mylevel, respectively, as long as mylevel is positive. This occurs until mylevel is 0, at which point the signal data_out is compared to the value stored in the variable data.
This complex example illustrates some of the challenges for the implementation of local variables. First, new copies of data and mylevel are needed for every cycle where there is a push to store their correct values at the cycle in question. However, there is variable delay from when data is assigned to when data is compared, and there can be any number of assignments to the variable mylevel in between. In the case of dynamic verification, there seems to be no way to determine in advance how many copies of the variables in question will be needed for an arbitrary trace. It doesn't seem feasible to compute a maximum number of copies sufficient to represent all the instances of possible overlap.
What is needed, therefore, is a static verification tool that can represent overlapping instances of a local variable without copying of variables during a static formal verification process.